First of all, you need to provide a module name. Module Code shall be defined as an abbreviation of your module name. For Syantax Panel, you have to fill in the language constructs of your new module, such as in CSP we support process interleave, parallel etc. The module generator will create these classes automatically for you.

As for Semantics panel here, we currently support three semantic models, e.g., LTS for CSP languages, TTS for timed systems and MDP for probabilistic systems. These are the three intermediate representations supported in PAT. After choosing the semantic model, the generator will automatically generate corresponding classes.

There are also a bunch of assertion checking algorithms supported and can be reused in the new module. Code will automatically generated according to the semantic model. You are also free to add domain specific assertions to your new module reusing these generated algorithms.

Note: if there is any error happened, try to regenerate the code again, since the code generation engine (from Microsoft) is not stable sometimes.

The following table summarizes the fields of the GUI to specify before generating codel.

Field Type	Optional	Field Name		Meaning	Remark	Example
Text box	No	Module  Name		Name	Name of the module	Event Grammar
	No	Module Code		Module Identifier	It will be used as the extention of the input file of the generated module.	EG
	Yes	Syntax		Language Construct	The generated code will contain a C# class for each language construct specified here.	Event, Process, Sentence, Sequence
Dropdown list	Choose one from the three	Semantic Model	LTS	Labeled Transition System	The generated module will first produce chosen semantic models and then execute corresponding model check algorithms on the semantic model.	Labeled Transition System (LTS)
			TTS	Timed Transition System
			MDP	Markov Decision Processes
Check box	NA	Generated BDD Encoding Methods		As named.	Tick this check box and the BDD encoding methods will be generated automatically, allowing developers to use PAT's BDD library for optimizing verification.	NA
		Supported Assertions	Deadlockfree		The interface of the deadlock checking algorithm will be generated.
			Reachability Checking		The interface of the state-reachability checking algorithm will be generated.
			Linear Temporal Logic		The interface of the LTL checking algorithm will be generated.
			Deterministic Checking		The interface of the deterministic checking algorithm will be generated.
			Divergence Checking		The interface of the Divergence checking algorithm will be generated.
			Refinement Checking		The interface of the refinement checking algorithm will be generated.